isl($x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $x$ of inl($y$) =$>$ tt $\mid$ inr($z$) =$>$ ff